
import java.io.BufferedWriter;
import java.util.Scanner;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;

/**
 * @author Stephen Bonsall
 * @date May 7
 */
public class Formula {
    private Scanner scannerFile;
    //stores formula
    private int [] [] formula;
	//each index in a clause specifies the variable.
	//1 for non negated, -1 for negated, 0 if the 
	//variable isnt present
	private int [][] soft_formula;
    //stores which clauses contain which variable
    private int NUMBER_OF_CLAUSES;
    private int NUMBER_OF_VARIABLES;

    /**
     * Constructor
     * @param filename
     */
    public Formula(String filename){

        try{
            scannerFile = new Scanner(new File(filename));
        }
        catch(IOException e){
            System.out.println("File does not exist");
        }

        createFormula();
    }

    /**
     * Constructor calls this method to create and set up all the lists
     */
    private void createFormula(){

        int clauseNum = 0;
        int variableNum = 0;
        NUMBER_OF_VARIABLES = 0;
        NUMBER_OF_CLAUSES = 0;

        String line = scannerFile.nextLine();

           //iterates through untill it finds the line that specifies
           //the number of variables and clauses
           while (!line.contains("p cnf")){
               line = scannerFile.nextLine();
           }

           String[] lineSplit = line.trim().split("\\s+");

           NUMBER_OF_VARIABLES = Integer.parseInt(lineSplit[2]);
           NUMBER_OF_CLAUSES = Integer.parseInt(lineSplit[3]);

           formula = new int[NUMBER_OF_CLAUSES][NUMBER_OF_VARIABLES];

           //enters each clause into the two-dimensional array
           while (scannerFile.hasNextLine()){
               line = scannerFile.nextLine();

               if(line.startsWith("c")){
               }

               else {

                   Scanner scannerLine = new Scanner(line.trim());
                   scannerLine.useDelimiter("\\s+");

                   while (scannerLine.hasNext()){
                            formula[clauseNum][variableNum] = 
                                    scannerLine.nextInt();
                            variableNum++;
                       }
                   }
               clauseNum++;
               variableNum = 0;
           }
    }


    public void printVHDLFormula(){
        try {
            int var = 1;
            BufferedWriter out = new BufferedWriter(new FileWriter("formula.vhdl"));
            out.write("library IEEE;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_1164.ALL;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_ARITH.ALL;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_UNSIGNED.ALL;");
            out.newLine();
            out.write("entity formula is");
            out.newLine();
            out.write("    port(");
            out.newLine();
            out.write("        enable: in std_logic;");
            out.newLine();
            out.write("        reset: in std_logic;");
            out.newLine();
            out.write("        a: in std_logic_vector(" +
                    (NUMBER_OF_VARIABLES - 1) +" downto 0);");
            out.newLine();
            out.write("        satisfied: out std_logic");
            out.newLine();
            out.write("    );");
            out.newLine();
            out.write("end entity formula;");
            out.newLine();
            out.write("architecture formula_behavior of formula is");
            out.newLine();
            out.write("signal sat_temp: std_logic := '0';");
            out.newLine();
            out.write("begin");
            out.newLine();
			out.write("process(enable, reset)");
			out.newLine();
			out.write("begin --process");
			out.newLine();
            out.write("    if enable = '1' and reset ='0' then");
            out.newLine();
            out.write("        if ");
            for (int i = 0; i < NUMBER_OF_CLAUSES; i++){
                out.write("(");
                var = formula[i][0];
                for (int j = 1; var != 0; j++){
                    if (var > 0){
                        out.write("a(" + (var-1) + ")='1'");
                    }
                    else if (var < 0){
                        var = var*-1;
                        out.write("a(" + (var-1) + ")='0'");
                    }
                    var = formula[i][j];
                    if(var == 0)
                        out.write(")");
                    else
                        out.write(" or ");

                }
                if(i == NUMBER_OF_CLAUSES -1)
                    out.write(" then");
                else
                    out.write(" and ");
            }
            out.newLine();
            out.write("            sat_temp <= '1';");
            out.newLine();
            out.write("       else");
            out.newLine();
            out.write("            sat_temp <= '0';");
            out.newLine();
            out.write("       end if;");
            out.newLine();
            out.write("    elsif reset = '1' then");
            out.newLine();
            out.write("        sat_temp <= '0';");
            out.newLine();
            out.write("    end if;");
            out.newLine();
            out.write("end process;");
            out.newLine();
            out.write("satisfied <= sat_temp;");
            out.newLine();
            out.write("end architecture formula_behavior;");

            out.close();
        } catch (IOException e) { }
    }

    public void printVHDLAssignments(){
        try{
			String ones = "";
            String zeroes = "";
            for(int i = 0; i < NUMBER_OF_VARIABLES; i++){
                zeroes = zeroes + "0";
				ones = ones + "1";
			}
            BufferedWriter out = new BufferedWriter(new FileWriter("assignment.vhdl"));
            out.write("library IEEE;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_1164.ALL;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_ARITH.ALL;");
            out.newLine();
            out.write("use IEEE.STD_LOGIC_UNSIGNED.ALL;");
            out.newLine();
            out.write("entity assignment is");
			out.newLine();
            out.write("    port(");
            out.newLine();
            out.write("        enable: in std_logic;");
            out.newLine();
            out.write("        reset: in std_logic;");
            out.newLine();
            out.write("        a: out std_logic_vector(" +
                    (NUMBER_OF_VARIABLES - 1) +" downto 0);");
            out.newLine();
			out.write("		 exhausted: out std_logic");
			out.newLine();
            out.write("    );");
            out.newLine();
            out.write("end assignment;");
            out.newLine();
            out.write("architecture assignment_behavior of assignment is");
            out.newLine();
            out.write("signal internal_assignment : std_logic_vector(" +
                    (NUMBER_OF_VARIABLES-1) + " downto 0) := \"" + zeroes + "\";");
			
			out.newLine();
            out.write("signal exhaust_temp : std_logic := '0';");
            out.newLine();
            out.write("begin");
            out.newLine();
            out.write("process(enable, reset)");
            out.newLine();
            out.write("begin");
            out.newLine();
            out.write("    if enable ='1' and reset='0' then");
            out.newLine();
            out.write("            internal_assignment <= internal_assignment + 1;");
            out.newLine();
            out.write("            if internal_assignment = \"" + ones +"\" then");
            out.newLine();
            out.write("                exhaust_temp <= '1';");
            out.newLine();
            out.write("            end if;");
            out.newLine();
            out.write("    elsif reset='1' then");
            out.newLine();
            out.write("        internal_assignment <= \"" + zeroes +"\";");
            out.newLine();
            out.write("        exhaust_temp <= '0';");
            out.newLine();
            out.write("    end if;");
            out.newLine();
            out.write("end process;");
            out.newLine();
            out.write("a <= internal_assignment;");
            out.newLine();
            out.write("exhausted <= exhaust_temp;");
            out.newLine();
            out.write("end architecture assignment_behavior;");
            out.close();
        }catch (IOException e) { }
    }
}



